/* Copyright 2013 Nicola Olivetti, Gian Luca Pozzato. This file is part of NESCOND.NESCOND is free software: you can redistribute it and/or modify it under the terms of the GNU General Public License as published by the Free Software Foundation, either version 3 of the License, or (at your option) any later version. NESCOND is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License for more details. You should have received a copy of the GNU General Public License along with NESCOND. If not, see . */ /* Automatic generator of formulas of NESCOND To test the performances of NESCOND for flat CK+CSO+ID and comparing them with the ones of KLMLean 2.0 for C, run: statistic(PosCond,NegCond,Proofs,Vars,Depth,MSec):- statistic(GoalVars,KBVars,DimKB,NumGoals,Depth,MSec) PosCond=number of positive conditionals NegCond=number of negative conditionals Proofs=number of tests Vars=number of different propositional variables Depth=maximun level of nesting of formulas MSec=timeout. */ :- op(400,fy,neg), op(400,fy,box), op(400,fy,l), op(500,xfy,and), op(600,xfy,or), op(650,xfy,->), op(650,xfy,=>). :- op(600,fy,!), op(500,xfy,=>), op(400,xfy,->), op(400,xfy,^), op(400,xfy,v). :-use_module(library(random)). :-use_module(library(lists)). :-use_module(library(timeout)). :-use_module(library(clpfd)). :-use_module(library(ordsets)). nth(1,[X|_],X):-!. nth(N,[_|Tail],Elem):-N1 is N-1,nth(N1,Tail,Elem). genProp(ATM,Var,0):-!,length(ATM,L),L1 is L+1,random(1,L1,Position),nth(Position,ATM,Var). genProp(ATM,Fml,Depth):-random(1,4,Rand),Depth1 is Depth - 1,genPropIn(ATM,Rand,Fml,Depth1). genPropIn(ATM,1,(A) and (B),Depth):-genProp(ATM,A,Depth),genProp(ATM,B,Depth). genPropIn(ATM,2,(A) or (B),Depth):-genProp(ATM,A,Depth),genProp(ATM,B,Depth). genPropIn(ATM,3,(A) -> (B),Depth):-genProp(ATM,A,Depth),genProp(ATM,B,Depth). genPropIn(ATM,4,neg (A),Depth):-genProp(ATM,A,Depth). genPosCond(ATM,(A) => (B),Depth):-genProp(ATM,A,Depth),genProp(ATM,B,Depth). genNegCond(ATM,neg((A) => (B)),Depth):-genProp(ATM,A,Depth),genProp(ATM,B,Depth). generateKnowledgeBase(PosCond,NegCond,ATM,Depth,KB):-!, generatePositiveConditionals(PosCond,ATM,Depth,KBPos), generateNegativeConditionals(NegCond,ATM,Depth,KBNeg), append(KBPos,KBNeg,KB). generatePositiveConditionals(0,_,_,[]):-!. generatePositiveConditionals(Dim,ATM,Depth,[Fml|KB]):- genPosCond(ATM,Fml,Depth), Dim1 is Dim-1, generatePositiveConditionals(Dim1,ATM,Depth,KB). generateNegativeConditionals(0,_,_,[]):-!. generateNegativeConditionals(Dim,ATM,Depth,[Fml|KB]):- genNegCond(ATM,Fml,Depth), Dim1 is Dim-1, generateNegativeConditionals(Dim1,ATM,Depth,KB). generateProofs(0,_,_,_,_,[]):-!. generateProofs(Proofs,PosCond,NegCond,ATM,Depth,[KB|ProofsTail]):- generateKnowledgeBase(PosCond,NegCond,ATM,Depth,KB), Proofs1 is Proofs-1, generateProofs(Proofs1,PosCond,NegCond,ATM,Depth,ProofsTail). generatePropVars(1,[p]):-!. generatePropVars(2,[p,q]):-!. generatePropVars(3,[p,q,r]):-!. generatePropVars(4,[p,q,r,p1]):-!. generatePropVars(5,[p,q,r,p1,q1]):-!. generatePropVars(6,[p,q,r,p1,q1,r1]):-!. generatePropVars(7,[p,q,r,p1,q1,r1,p2]):-!. generatePropVars(8,[p,q,r,p1,q1,r1,p2,q2]):-!. generatePropVars(9,[p,q,r,p1,q1,r1,p2,q2,r2]):-!. generatePropVars(10,[p,q,r,p1,q1,r1,p2,q2,r2,p3]):-!. generatePropVars(11,[p,q,r,p1,q1,r1,p2,q2,r2,p3,q3]):-!. generatePropVars(12,[p,q,r,p1,q1,r1,p2,q2,r2,p3,q3,r3]):-!. generatePropVars(13,[p,q,r,p1,q1,r1,p2,q2,r2,p3,q3,r3,p4]):-!. generatePropVars(14,[p,q,r,p1,q1,r1,p2,q2,r2,p3,q3,r3,p4,q4]):-!. generatePropVars(15,[p,q,r,p1,q1,r1,p2,q2,r2,p3,q3,r3,p4,q4,r4]):-!. generatePropVars(16,[p,q,r,p1,q1,r1,p2,q2,r2,p3,q3,r3,p4,q4,r4,p5]):-!. generatePropVars(17,[p,q,r,p1,q1,r1,p2,q2,r2,p3,q3,r3,p4,q4,r4,p5,q5]):-!. generatePropVars(18,[p,q,r,p1,q1,r1,p2,q2,r2,p3,q3,r3,p4,q4,r4,p5,q5,r5]):-!. generatePropVars(19,[p,q,r,p1,q1,r1,p2,q2,r2,p3,q3,r3,p4,q4,r4,p5,q5,r5,s]):-!. generatePropVars(20,[p,q,r,p1,q1,r1,p2,q2,r2,p3,q3,r3,p4,q4,r4,p5,q5,r5,s,t]):-!. statistic(PosCond,NegCond,Proofs,Vars,Depth,MSec):- retractall(succStandard(_)), retractall(timeStandard(_)), retractall(succNESCOND(_)), retractall(timeNESCOND(_)), asserta(succStandard(0)), asserta(timeStandard(0)), asserta(succNESCOND(0)), asserta(timeNESCOND(0)), generatePropVars(Vars,ATM), generateProofs(Proofs,PosCond,NegCond,ATM,Depth,KB), executeStandard(KB,MSec), succStandard(NL), timeStandard(TL), FL is Proofs-NL-TL, changeConnectives(KB,KBP), executeNESCOND(KBP,MSec), succNESCOND(NA), timeNESCOND(TA), FA is Proofs-NA-TA, write('\n'), write('Riassunto: S T N\n'), write('KLMLean 2.0 '),write(NL),write(' '),write(TL),write(' '),write(FL),write('\n'), write('NESCOND '),write(NA),write(' '),write(TA),write(' '),write(FA),write('\n'). /* Convert KLM formulas to CK+ID+CSO formulas */ changeConnectives([],[]):-!. changeConnectives([Head|Tail],[CH|ResTail]):-convertFml(Head,CH),changeConnectives(Tail,ResTail). convertFml([],[]):-!. convertFml([Fml|Tail],[CF|ResTail]):-convertSingleFml(Fml,CF),convertFml(Tail,ResTail). convertSingleFml((A) and (B),(AC) ^ (BC)):-!,convertSingleFml(A,AC),convertSingleFml(B,BC). convertSingleFml((A) or (B),(AC) v (BC)):-!,convertSingleFml(A,AC),convertSingleFml(B,BC). convertSingleFml(neg (A),!(AC)):-!,convertSingleFml(A,AC). convertSingleFml(F,F):-!. executeStandard([],_):-!. executeStandard([KB|Tail],MSec):- ( time_out( ( prove(KB,[],_,[]) ),MSec,Result),!, ( ( Result=success,!, succStandard(N),retractall(succStandard(_)),N1 is N+1,asserta(succStandard(N1)), executeStandard(Tail,MSec) ); ( timeStandard(T),retractall(timeStandard(_)),T1 is T+1,asserta(timeStandard(T1)), executeStandard(Tail,MSec) ) ) ) ; executeStandard(Tail,MSec). executeNESCOND([],_):-!. executeNESCOND([KB|Tail],MSec):- ( time_out( ( proveNS(KB,_) ),MSec,Result),!, ( ( Result=success,!, succNESCOND(N),retractall(succNESCOND(_)),N1 is N+1,asserta(succNESCOND(N1)), executeNESCOND(Tail,MSec) ); ( timeNESCOND(T),retractall(timeNESCOND(_)),T1 is T+1,asserta(timeNESCOND(T1)), executeNESCOND(Tail,MSec) ) ) ) ; executeNESCOND(Tail,MSec). /* Auxiliary predicate computing \Gamma^M_{x -> y} */ gammaM([],_,_,[]):-!. gammaM([[X,box A]|Tail],X,Y,[[Y,A]|[[Y,box A]|ResTail]]):-!,gammaM(Tail,X,Y,ResTail). gammaM([_|Tail],X,Y,ResTail):-gammaM(Tail,X,Y,ResTail). /* Predicates used to estimate the degree of utility of a conditional formula */ maxDegree(Gamma,Labels,Cond,[X,A => B],Max):- labelConditionals(Gamma,Labels,ListOfConditionals), filterAlreadyAppliedConditionals(ListOfConditionals,Cond,ListOfAvailableConditionals), eachDegree(Gamma,ListOfAvailableConditionals,ListOfDegrees), findMax(ListOfDegrees,Max,Position),!, nth(Position,ListOfAvailableConditionals,[X,A => B]). /* Given the list of all possible labelled positive conditionals, and given the list of conditionals to which (|~+) has already been applied in the current branch, this predicate returns the list of available conditionals, i.e. those ones to what the above rule can still be applied */ filterAlreadyAppliedConditionals([],_,[]):-!. filterAlreadyAppliedConditionals([F|Tail],Cond,ResTail):- member(F,Cond),!,filterAlreadyAppliedConditionals(Tail,Cond,ResTail). filterAlreadyAppliedConditionals([F|Tail],Cond,[F|ResTail]):- filterAlreadyAppliedConditionals(Tail,Cond,ResTail). eachDegree(_,[],[]):-!. eachDegree(Gamma,[[X,A => B]|TailCond],[CurrentDegree|TailDeg]):-!, evaluateDegree([X,A => B],Gamma,CurrentDegree), eachDegree(Gamma,TailCond,TailDeg). evaluateDegree([X,A => B],Gamma,Deg):- ( (member([X,neg A],Gamma);member([X,neg box neg A],Gamma);member([X,B],Gamma)), Deg is 0 ) ; ( firstEval([X,A => B],Gamma,Res1), secondEval([X,A => B],Gamma,Res2), thirdEval([X,A => B],Gamma,Res3), Deg is Res1+Res2+Res3 ). firstEval([X,A => _],Gamma,Val):- (member([X,box neg A],Gamma),Val is 12);Val is 1. secondEval([X,A => _],Gamma,Val):- (member([X,A],Gamma),Val is 5);Val is 1. thirdEval([X,_ => B],Gamma,Val):- (member([X,neg B],Gamma),Val is 5);Val is 1. labelConditionals([],_,[]):-!. labelConditionals([[_,A => B]|Tail],Labels,Result):-!, labelSingleConditional(A => B,Labels,InstancesOfCurrentConditional), labelConditionals(Tail,Labels,ResTail), append(InstancesOfCurrentConditional,ResTail,Result). labelConditionals([_|Tail],Labels,Result):-labelConditionals(Tail,Labels,Result). labelSingleConditional(_,[],[]):-!. labelSingleConditional(A => B,[X|LabTail],[[X,A => B]|CondTail]):-!, labelSingleConditional(A => B,LabTail,CondTail). findMax([],0,0):-!. findMax([Current|Tail],Max,Position):- findMax(Tail,MaxTail,PosMaxInTail),!, ((Current > MaxTail,Max is Current,Position is 1) ; (Position is 1+PosMaxInTail,Max is MaxTail)). /* Generates a new label */ newLabel([],x). newLabel([x],y). newLabel([y,x],z). newLabel([z,y,x],u). newLabel([u,z,y,x],v). newLabel([v,u,z,y,x],w). newLabel([w,v,u,z,y,x],x+1). newLabel([x+N|_],x+N1):-N1 is N+1. /* ---------------------------------------------------------------- */ /* ---------------------------------------------------------------- */ /* The following predicates implement KLMLean 2.0 for C - standard version */ /* ---------------------------------------------------------------- */ /* ---------------------------------------------------------------- */ /* The following predicate implements the calculi: prove(Gamma,[],Tree,Analyzed) iff there exists a closed tableaux Tree for Gamma;\emptyset */ prove(Gamma,Sigma,Tree,Analyzed):- append(Gamma,Sigma,Node), list_to_ord_set(Node,Current), \+ord_member(Current,Analyzed), ord_add_element(Analyzed,Current,NewAnalyzed), proveStandard(Gamma,Sigma,Tree,NewAnalyzed). proveStandard(Gamma,_,tree(ax,F),_):- member(neg F,Gamma),member(F, Gamma),!. proveStandard(Gamma,Sigma,tree(andP,F,G,ST),Analyzed):- select(F and G,Gamma,NewGamma),!, prove([F|[G|NewGamma]],Sigma,ST,Analyzed). proveStandard(Gamma,Sigma,tree(orN,F,G,ST),Analyzed):- select(neg (F or G),Gamma,NewGamma),!, prove([neg F|[neg G|NewGamma]],Sigma,ST,Analyzed). proveStandard(Gamma,Sigma,tree(impN,F,G,ST),Analyzed):- select(neg (F -> G),Gamma,NewGamma),!, prove([F|[neg G|NewGamma]],Sigma,ST,Analyzed). proveStandard(Gamma,Sigma,tree(neg,F,ST),Analyzed):- select(neg neg F,Gamma,NewGamma),!, prove([F|NewGamma],Sigma,ST,Analyzed). proveStandard(Gamma,Sigma,tree(andN,F,G,ST1,ST2),Analyzed):- select(neg (F and G),Gamma,NewGamma),!, prove([neg F|NewGamma],Sigma,ST1,Analyzed),!, prove([neg G|NewGamma],Sigma,ST2,Analyzed). proveStandard(Gamma,Sigma,tree(orP,F,G,ST1,ST2),Analyzed):- select(F or G,Gamma,NewGamma),!, prove([F|NewGamma],Sigma,ST1,Analyzed),!, prove([G|NewGamma],Sigma,ST2,Analyzed). proveStandard(Gamma,Sigma,tree(impP,F,G,ST1,ST2),Analyzed):- select(F -> G,Gamma,NewGamma),!, prove([neg F|NewGamma],Sigma,ST1,Analyzed),!, prove([G|NewGamma],Sigma,ST2,Analyzed). proveStandard(Gamma,Sigma,tree(entN,A,B,ST),Analyzed):- select(neg (A => B),Gamma,NewGamma), conditionals(NewGamma,CondGamma), append(Sigma,CondGamma,DefGamma), prove([l A|[box neg l A|[neg l B|DefGamma]]],[],ST,Analyzed). /* Remark: as a difference from the rule (|~+) presented in the papers, having 3 conclusions, KLMLean 2.0 implements an equivalent one having only two conclusions: \Gamma, A |~ B \Gamma, A |~ B ------------------------------------- --------------------------------------------- (1) \Gamma, A |~ B, ~LA (1) ..., A |~ B, LA, []~LA (2) ..., A |~ B, LA, []~LA (2) \Gamma, A |~ B, LA -> (LA & []~LA & LB) (3) \Gamma, A |~ B, LA, []~LA, LB This chioce has been made in order to simplify the graphical user interface, displaying only binary trees. */ proveStandard(Gamma,Sigma,tree(entP,A,B,ST1,ST2),Analyzed):- select(A => B,Gamma,NewGamma), conditionals(NewGamma,Cond), inboxed(NewGamma,InBoxed), append(Cond,InBoxed,Gammastar), append(Gammastar,Sigma,DefGammaLeft), prove([box neg l A|[l A|[A => B|DefGammaLeft]]],[],ST1,Analyzed), prove([(l A) -> (l A and box neg l A and l B)|NewGamma],[A => B|Sigma],ST2,Analyzed). proveStandard(Gamma,_,tree(elleN,A,ST),Analyzed):- select(neg l A,Gamma,NewGamma), inelle(NewGamma,DefGamma), prove([neg A|DefGamma],[],ST,Analyzed). proveStandard(Gamma,_,tree(elleN,ST),Analyzed):- inelle(Gamma,DefGamma), prove(DefGamma,[],ST,Analyzed). /* Auxiliary predicates */ inelle([],[]):-!. inelle([l A|Tail],[A|ResTail]):-!,inelle(Tail,ResTail). inelle([_|Tail],ResTail):-!,inelle(Tail,ResTail). conditionals([],[]):-!. conditionals([A => B|Tail],[A => B|CondTail]):-!,conditionals(Tail,CondTail). conditionals([neg (A => B)|Tail],[neg (A => B)|CondTail]):-!,conditionals(Tail,CondTail). conditionals([_|Tail],CondTail):-conditionals(Tail,CondTail). inboxed([],[]):-!. inboxed([box A|Tail],[A|InBoxTail]):-!,inboxed(Tail,InBoxTail). inboxed([_|Tail],InBoxTail):-inboxed(Tail,InBoxTail). /* Prove: benissimo: statistic(3,3,20,5,3,100). bene: statistic(5,10,20,5,3,100). statistic(5,15,20,5,3,100). Con tanti soddisfacibili: statistic(3,3,50,5,2,1). statistic(3,3,100,7,2,1). */ /* ---------------------------------------------------------------- */ /* ---------------------------------------------------------------- */ /* The following predicates implement NESCOND for CK+ID+CSO */ /* ---------------------------------------------------------------- */ /* ---------------------------------------------------------------- */ fillTheHole(NS,ListToFill,NewNS):-select(hole,NS,TempNS),!, append(TempNS,ListToFill,NewNS). fillTheHole(NS,ListToFill,[[[Fml,NewGamma],AppliedConditionals,AllowID]|TempNS]):-select([[Fml,Gamma],AppliedConditionals,AllowID],NS,TempNS), fillTheHole(Gamma,ListToFill,NewGamma). selectList([],NS,[hole|NS]). selectList([Fml|Tail],NS,NewNS):-select(Fml,NS,TempNS), selectList(Tail,TempNS,NewNS). deepSelect(List,NS,NewNS):-selectList(List,NS,NewNS). deepSelect(List,NS,[[[Fml,NewGamma],AppliedConditionals,AllowID]|NewNS]):-select([[Fml,Gamma],AppliedConditionals,AllowID],NS,NewNS), deepSelect(List,Gamma,NewGamma). memberList([],_). memberList([Head|Tail],NS):-member(Head,NS),memberList(Tail,NS). deepMember(List,NS):-memberList(List,NS). deepMember(List,NS):-member([[_,Gamma],_,_],NS), deepMember(List,Gamma). /* Axioms closing branches */ proveNS(NS,tree(ax)):-deepMember([P,!P],NS),!. proveNS(NS,tree(axt)):-deepMember([top],NS),!. proveNS(NS,tree(axb)):-deepMember([!bot],NS),!. /* Rules with one premise */ proveNS(NS,tree(neg,A,SubTree)):-deepSelect([!!A],NS,NewNS),!,fillTheHole(NewNS,[A],DefNS),proveNS(DefNS,SubTree). proveNS(NS,tree(orp,A,B,SubTree)):-deepSelect([A v B],NS,NewNS),!,fillTheHole(NewNS,[A,B],DefNS),proveNS(DefNS,SubTree). proveNS(NS,tree(andn,A,B,SubTree)):-deepSelect([!(A ^ B)],NS,NewNS),!,fillTheHole(NewNS,[!A,!B],DefNS),proveNS(DefNS,SubTree). proveNS(NS,tree(impp,A,B,SubTree)):-deepSelect([A -> B],NS,NewNS),!,fillTheHole(NewNS,[!A,B],DefNS),proveNS(DefNS,SubTree). proveNS(NS,tree(condp,A,B,SubTree)):-deepSelect([A => B],NS,NewNS),!,fillTheHole(NewNS,[[[A,[B]],[],true]],DefNS),proveNS(DefNS,SubTree). proveNS(NS,tree(id,A,SubTree)):-deepSelect([[[A,Delta],AppliedConditionals,true]],NS,NewNS),!, fillTheHole(NewNS,[[[A,[!A|Delta]],AppliedConditionals,false]],DefNS), proveNS(DefNS,SubTree). /* Rules with two or three premises (introducing a branch in a backward proof search) */ proveNS(NS,tree(orn,A,B,Sub1,Sub2)):-deepSelect([!(A v B)],NS,NewNS),!,fillTheHole(NewNS,[!A],NS1),fillTheHole(NewNS,[!B],NS2),proveNS(NS1,Sub1),proveNS(NS2,Sub2). proveNS(NS,tree(andp,A,B,Sub1,Sub2)):-deepSelect([A ^ B],NS,NewNS),!,fillTheHole(NewNS,[A],NS1),fillTheHole(NewNS,[B],NS2),proveNS(NS1,Sub1),proveNS(NS2,Sub2). proveNS(NS,tree(impn,A,B,Sub1,Sub2)):-deepSelect([!(A -> B)],NS,NewNS),!,fillTheHole(NewNS,[A],NS1),fillTheHole(NewNS,[!B],NS2),proveNS(NS1,Sub1),proveNS(NS2,Sub2). proveNS(NS,tree(cso,A,B,Sub1,Sub2,Sub3)):- member(!(A => B),NS), select([[C,Delta],AppliedConditionals,AllowID],NS,NewNS), \+member(!(A => B),AppliedConditionals), proveNS([[[C,[A]],[],true]|NewNS],Sub1), proveNS([[[A,[C]],[],true]|NewNS],Sub2), proveNS([[[C,[(!B)|Delta]],[!(A => B)|AppliedConditionals],AllowID]|NewNS],Sub3). /* Predicates to compare KLMLean and NESCOND over valid formulas */ listOfValid([((a => b1) and (a => c)) -> ((a and b1) => c), ((a => b1) and (a => b2) and (a => c)) -> ((a and b1 and b2) => c), ((a => b1) and (a => b2) and (a => b3) and (a => c)) -> ((a and b1 and b2 and b3) => c), ((a => b1) and (a => b2) and (a => b3) and (a => b4) and (a => c)) -> ((a and b1 and b2 and b3 and b4) => c), ((a => b1) and (a => b2) and (a => b3) and (a => b4) and (a => b5) and (a => c)) -> ((a and b1 and b2 and b3 and b4 and b5) => c), ((a => b1) and (a => b2) and (a => b3) and (a => b4) and (a => b5) and (a => b6) and (a => c)) -> ((a and b1 and b2 and b3 and b4 and b5 and b6) => c), ((a => b1) and (a => b2) and (a => b3) and (a => b4) and (a => b5) and (a => b6) and (a => b7) and (a => c)) -> ((a and b1 and b2 and b3 and b4 and b5 and b6 and b7) => c), ((a => b1) and (a => b2) and (a => b3) and (a => b4) and (a => b5) and (a => b6) and (a => b7) and (a => b8) and (a => c)) -> ((a and b1 and b2 and b3 and b4 and b5 and b6 and b7 and b8) => c), ((a => b1) and (a => b2) and (a => b3) and (a => b4) and (a => b5) and (a => b6) and (a => b7) and (a => b8) and (a => b9) and (a => c)) -> ((a and b1 and b2 and b3 and b4 and b5 and b6 and b7 and b8 and b9) => c), ((a => b1) and ((a and b1) => c)) -> (a => c), ((a => b1) and (a => b2) and ((a and b1 and b2) => c)) -> (a => c), ((a => b1) and (a => b2) and (a => b3) and ((a and b1 and b2 and b3) => c)) -> (a => c), ((a => b1) and (a => b2) and (a => b3) and (a => b4) and ((a and b1 and b2 and b3 and b4) => c)) -> (a => c), ((a => b1) and (a => b2) and (a => b3) and (a => b4) and (a => b5) and ((a and b1 and b2 and b3 and b4 and b5) => c)) -> (a => c), ((a => b1) and (a => b2) and (a => b3) and (a => b4) and (a => b5) and (a => b6) and ((a and b1 and b2 and b3 and b4 and b5 and b6) => c)) -> (a => c), ((a => b1) and (a => b2) and (a => b3) and (a => b4) and (a => b5) and (a => b6) and (a => b7) and ((a and b1 and b2 and b3 and b4 and b5 and b6 and b7) => c)) -> (a => c), ((a => b1) and (a => b2) and (a => b3) and (a => b4) and (a => b5) and (a => b6) and (a => b7) and (a => b8) and ((a and b1 and b2 and b3 and b4 and b5 and b6 and b7 and b8) => c)) -> (a => c), ((a => b1) and (a => b2) and (a => b3) and (a => b4) and (a => b5) and (a => b6) and (a => b7) and (a => b8) and (a => b9) and ((a and b1 and b2 and b3 and b4 and b5 and b6 and b7 and b8 and b9) => c)) -> (a => c), ((a => b1) and (a => b2) and (a => b3) and (a => b4) and (a => b5) and (a => b6) and (a => b7) and (a => b8) and (a => b9) and (a => b10) and ((a and b1 and b2 and b3 and b4 and b5 and b6 and b7 and b8 and b9 and b10) => c)) -> (a => c), ((a1 => a2) and (a2 => a1) and (a1 => c)) -> (a2 => c), ((a1 => a2) and (a2 => a1) and (a2 => a3) and (a3 => a2) and (a1 => c)) -> (a3 => c), ((a1 => a2) and (a2 => a1) and (a2 => a3) and (a3 => a2) and (a3 => a4) and (a4 => a3) and (a1 => c)) -> (a4 => c), ((a1 => a2) and (a2 => a1) and (a2 => a3) and (a3 => a2) and (a3 => a4) and (a4 => a3) and (a4 => a5) and (a5 => a4) and (a1 => c)) -> (a5 => c), ((a1 => a2) and (a2 => a1) and (a2 => a3) and (a3 => a2) and (a3 => a4) and (a4 => a3) and (a4 => a5) and (a5 => a4) and (a5 => a6) and (a6 => a5) and (a1 => c)) -> (a6 => c), ((a1 => a2) and (a2 => a1) and (a2 => a3) and (a3 => a2) and (a3 => a4) and (a4 => a3) and (a4 => a5) and (a5 => a4) and (a5 => a6) and (a6 => a5) and (a6 => a7) and (a7 => a6) and (a1 => c)) -> (a7 => c), ((a1 => a2) and (a2 => a1) and (a2 => a3) and (a3 => a2) and (a3 => a4) and (a4 => a3) and (a4 => a5) and (a5 => a4) and (a5 => a6) and (a6 => a5) and (a6 => a7) and (a7 => a6) and (a7 => a8) and (a8 => a7) and (a1 => c)) -> (a8 => c)]). listOfValidNESCOND([((a => b1) ^ (a => c)) -> ((a ^ b1) => c), ((a => b1) ^ (a => b2) ^ (a => c)) -> ((a ^ b1 ^ b2) => c), ((a => b1) ^ (a => b2) ^ (a => b3) ^ (a => c)) -> ((a ^ b1 ^ b2 ^ b3) => c), ((a => b1) ^ (a => b2) ^ (a => b3) ^ (a => b4) ^ (a => c)) -> ((a ^ b1 ^ b2 ^ b3 ^ b4) => c), ((a => b1) ^ (a => b2) ^ (a => b3) ^ (a => b4) ^ (a => b5) ^ (a => c)) -> ((a ^ b1 ^ b2 ^ b3 ^ b4 ^ b5) => c), ((a => b1) ^ (a => b2) ^ (a => b3) ^ (a => b4) ^ (a => b5) ^ (a => b6) ^ (a => c)) -> ((a ^ b1 ^ b2 ^ b3 ^ b4 ^ b5 ^ b6) => c), ((a => b1) ^ (a => b2) ^ (a => b3) ^ (a => b4) ^ (a => b5) ^ (a => b6) ^ (a => b7) ^ (a => c)) -> ((a ^ b1 ^ b2 ^ b3 ^ b4 ^ b5 ^ b6 ^ b7) => c), ((a => b1) ^ (a => b2) ^ (a => b3) ^ (a => b4) ^ (a => b5) ^ (a => b6) ^ (a => b7) ^ (a => b8) ^ (a => c)) -> ((a ^ b1 ^ b2 ^ b3 ^ b4 ^ b5 ^ b6 ^ b7 ^ b8) => c), ((a => b1) ^ (a => b2) ^ (a => b3) ^ (a => b4) ^ (a => b5) ^ (a => b6) ^ (a => b7) ^ (a => b8) ^ (a => b9) ^ (a => c)) -> ((a ^ b1 ^ b2 ^ b3 ^ b4 ^ b5 ^ b6 ^ b7 ^ b8 ^ b9) => c), ((a => b1) ^ ((a ^ b1) => c)) -> (a => c), ((a => b1) ^ (a => b2) ^ ((a ^ b1 ^ b2) => c)) -> (a => c), ((a => b1) ^ (a => b2) ^ (a => b3) ^ ((a ^ b1 ^ b2 ^ b3) => c)) -> (a => c), ((a => b1) ^ (a => b2) ^ (a => b3) ^ (a => b4) ^ ((a ^ b1 ^ b2 ^ b3 ^ b4) => c)) -> (a => c), ((a => b1) ^ (a => b2) ^ (a => b3) ^ (a => b4) ^ (a => b5) ^ ((a ^ b1 ^ b2 ^ b3 ^ b4 ^ b5) => c)) -> (a => c), ((a => b1) ^ (a => b2) ^ (a => b3) ^ (a => b4) ^ (a => b5) ^ (a => b6) ^ ((a ^ b1 ^ b2 ^ b3 ^ b4 ^ b5 ^ b6) => c)) -> (a => c), ((a => b1) ^ (a => b2) ^ (a => b3) ^ (a => b4) ^ (a => b5) ^ (a => b6) ^ (a => b7) ^ ((a ^ b1 ^ b2 ^ b3 ^ b4 ^ b5 ^ b6 ^ b7) => c)) -> (a => c), ((a => b1) ^ (a => b2) ^ (a => b3) ^ (a => b4) ^ (a => b5) ^ (a => b6) ^ (a => b7) ^ (a => b8) ^ ((a ^ b1 ^ b2 ^ b3 ^ b4 ^ b5 ^ b6 ^ b7 ^ b8) => c)) -> (a => c), ((a => b1) ^ (a => b2) ^ (a => b3) ^ (a => b4) ^ (a => b5) ^ (a => b6) ^ (a => b7) ^ (a => b8) ^ (a => b9) ^ ((a ^ b1 ^ b2 ^ b3 ^ b4 ^ b5 ^ b6 ^ b7 ^ b8 ^ b9) => c)) -> (a => c), ((a => b1) ^ (a => b2) ^ (a => b3) ^ (a => b4) ^ (a => b5) ^ (a => b6) ^ (a => b7) ^ (a => b8) ^ (a => b9) ^ (a => b10) ^ ((a ^ b1 ^ b2 ^ b3 ^ b4 ^ b5 ^ b6 ^ b7 ^ b8 ^ b9 ^ b10) => c)) -> (a => c), ((a1 => a2) ^ (a2 => a1) ^ (a1 => c)) -> (a2 => c), ((a1 => a2) ^ (a2 => a1) ^ (a2 => a3) ^ (a3 => a2) ^ (a1 => c)) -> (a3 => c), ((a1 => a2) ^ (a2 => a1) ^ (a2 => a3) ^ (a3 => a2) ^ (a3 => a4) ^ (a4 => a3) ^ (a1 => c)) -> (a4 => c), ((a1 => a2) ^ (a2 => a1) ^ (a2 => a3) ^ (a3 => a2) ^ (a3 => a4) ^ (a4 => a3) ^ (a4 => a5) ^ (a5 => a4) ^ (a1 => c)) -> (a5 => c), ((a1 => a2) ^ (a2 => a1) ^ (a2 => a3) ^ (a3 => a2) ^ (a3 => a4) ^ (a4 => a3) ^ (a4 => a5) ^ (a5 => a4) ^ (a5 => a6) ^ (a6 => a5) ^ (a1 => c)) -> (a6 => c), ((a1 => a2) ^ (a2 => a1) ^ (a2 => a3) ^ (a3 => a2) ^ (a3 => a4) ^ (a4 => a3) ^ (a4 => a5) ^ (a5 => a4) ^ (a5 => a6) ^ (a6 => a5) ^ (a6 => a7) ^ (a7 => a6) ^ (a1 => c)) -> (a7 => c), ((a1 => a2) ^ (a2 => a1) ^ (a2 => a3) ^ (a3 => a2) ^ (a3 => a4) ^ (a4 => a3) ^ (a4 => a5) ^ (a5 => a4) ^ (a5 => a6) ^ (a6 => a5) ^ (a6 => a7) ^ (a7 => a6) ^ (a7 => a8) ^ (a8 => a7) ^ (a1 => c)) -> (a8 => c) ]). testOnValid(MSec):- retractall(succStandard(_)), retractall(timeStandard(_)), retractall(succNESCOND(_)), retractall(timeNESCOND(_)), asserta(succStandard(0)), asserta(timeStandard(0)), asserta(succNESCOND(0)), asserta(timeNESCOND(0)), listOfValid(KB), validKLM(KB,MSec), succStandard(NL), timeStandard(TL), length(KB,Proofs), FL is Proofs-NL-TL, listOfValidNESCOND(KBP), validNESCOND(KBP,MSec), succNESCOND(NA), timeNESCOND(TA), FA is Proofs-NA-TA, write('\n'), write('Riassunto: S T N\n'), write('KLMLean 2.0 '),write(NL),write(' '),write(TL),write(' '),write(FL),write('\n'), write('NESCOND '),write(NA),write(' '),write(TA),write(' '),write(FA),write('\n'). validKLM([],_):-!. validKLM([KB|Tail],MSec):- ( time_out( ( prove([neg KB],[],_,[]) ),MSec,Result),!, ( ( Result=success,!, succStandard(N),retractall(succStandard(_)),N1 is N+1,asserta(succStandard(N1)), validKLM(Tail,MSec) ); ( timeStandard(T),retractall(timeStandard(_)),T1 is T+1,asserta(timeStandard(T1)), validKLM(Tail,MSec) ) ) ) ; validKLM(Tail,MSec). validNESCOND([],_):-!. validNESCOND([KB|Tail],MSec):- ( time_out( ( proveNS([KB],_) ),MSec,Result),!, ( ( Result=success,!, succNESCOND(N),retractall(succNESCOND(_)),N1 is N+1,asserta(succNESCOND(N1)), validNESCOND(Tail,MSec) ); ( timeNESCOND(T),retractall(timeNESCOND(_)),T1 is T+1,asserta(timeNESCOND(T1)), validNESCOND(Tail,MSec) ) ) ) ; validNESCOND(Tail,MSec).